\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it es}$:event\_system\{i:l\}, $i$:Id,\+
\\[0ex]${\it LL}$:(event{-}info(${\it ds}$;${\it da}$) List List), $e_{1}$,$e_{2}$:\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = $i$\} ,
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]l\_all(${\it LL}$; (event{-}info(${\it ds}$;${\it da}$) List); $L$.($\neg$($L$ = [])))
\\[0ex]$\Rightarrow$ ($\neg$($L$ = []))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; $e$); top)))
\-\\[0ex]$\Rightarrow$ (es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$) = append(concat(${\it LL}$); $L$) $\in$ (event{-}info(${\it ds}$;${\it da}$) List))
\\[0ex]$\Rightarrow$ ($\exists$\=$f$:int\_seg(0; ($\parallel$${\it LL}$$\parallel$ + 1))$\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = $i$\} \+
\\[0ex]((($f$(0) = $e_{1}$) $\wedge$ es{-}le(${\it es}$; ($f$($\parallel$${\it LL}$$\parallel$)); $e_{2}$))
\\[0ex]c$\wedge$ ($\forall$$i$:int\_seg(0; $\parallel$${\it LL}$$\parallel$). es{-}locl(${\it es}$; ($f$($i$)); ($f$($i$ + 1))))
\\[0ex]c$\wedge$ \=(($\forall$$i$:int\_seg(0; $\parallel$${\it LL}$$\parallel$). \+
\\[0ex]es{-}hist\{i:l\}(${\it es}$;$f$($i$);es{-}pred(${\it es}$; ($f$($i$ + 1)))) = ${\it LL}$[$i$] $\in$ (event{-}info(${\it ds}$;${\it da}$) List))
\\[0ex]$\wedge$ (es{-}hist\{i:l\}(${\it es}$;$f$($\parallel$${\it LL}$$\parallel$);$e_{2}$) = $L$))))
\-\-
\end{tabbing}